\begin{tabbing}
$\forall$\=$i$:Id, $k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type,\+
\\[0ex]$f$:(${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(${\it da}$(rcv($l$,${\it tg}$))?Void List))) List.
\-\\[0ex]source($l$) $=$ $i$
\\[0ex]$\Rightarrow$ \=@$i$: with declarations ds:${\it ds}$da:${\it da}$$k$(v) sends $f$ s v on link $l$ $\in$ Dsys\+
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: with declarations ds:${\it ds}$da:${\it da}$$k$(v) sends $f$ s v on link $l$ $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]\& ($\forall$$e$:E. loc($e$) $=$ $i$ $\in$ Id $\Rightarrow$ valtype($e$) $\subseteq\rho$ Valtype(${\it da}$;kind($e$)))
\\[0ex]\& ($\forall$$e$:E. isrcv($e$) $\Rightarrow$ lnk($e$) $=$ $l$ $\in$ IdLnk $\Rightarrow$ valtype($e$) $\subseteq\rho$ Valtype(${\it da}$;kind($e$)))
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ $i$ $\in$ Id
\\[0ex]$\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ (\=$\exists$$L$:\{${\it e'}$:E$\mid$ isrcv(${\it e'}$) \& lnk(${\it e'}$) $=$ $l$ $\in$ IdLnk \} List.\+
\\[0ex]($\forall$${\it e'}$:E. (${\it e'}$ $\in$ $L$) $\Leftrightarrow$ isrcv(${\it e'}$) \& lnk(${\it e'}$) $=$ $l$ $\in$ IdLnk \& sender(${\it e'}$) $=$ $e$ $\in$ E)
\\[0ex]\& ($\forall$$e_{1}$, $e_{2}$:E. $e_{1}$ before $e_{2}$ $\in$ $L$ $\Rightarrow$ ($e_{1}$ $<$loc $e_{2}$))
\\[0ex]\& \=map($\lambda$${\it e'}$.$\langle$tag(${\it e'}$)$,\,$val(${\it e'}$)$\rangle$;$L$)\+
\\[0ex]$=$
\\[0ex]tagged{-}list{-}messages($\lambda$$z$.$z$ when $e$;val($e$);$f$)
\\[0ex]$\in$ (${\it tg}$:Id$\times$Valtype(${\it da}$;rcv($l$,${\it tg}$))) List)))
\-\-\-\-\-\-
\end{tabbing}